The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 358 ms)
    ↳6 CdtProblem
    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 70 ms)
    ↳12 CdtProblem
    ↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 76 ms)
    ↳14 CdtProblem
    ↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 207 ms)
    ↳20 CdtProblem
    ↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳22 CdtProblem
    ↳23 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳24 CdtProblem
    ↳25 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳26 CdtProblem
    ↳27 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳28 CdtProblem
↳29 CpxTrsMatchBoundsTAProof (⇔, 44 ms)
↳30 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

ACTIVE(f(z0, z0)) → c(MARK(f(a, b)), F(a, b))
ACTIVE(b) → c1(MARK(a))
MARK(f(z0, z1)) → c2(ACTIVE(f(mark(z0), z1)), F(mark(z0), z1), MARK(z0))
MARK(a) → c3(ACTIVE(a))
MARK(b) → c4(ACTIVE(b))
F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
S tuples:

ACTIVE(f(z0, z0)) → c(MARK(f(a, b)), F(a, b))
ACTIVE(b) → c1(MARK(a))
MARK(f(z0, z1)) → c2(ACTIVE(f(mark(z0), z1)), F(mark(z0), z1), MARK(z0))
MARK(a) → c3(ACTIVE(a))
MARK(b) → c4(ACTIVE(b))
F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
K tuples:none
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, MARK, F

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 3 trailing nodes:

MARK(a) → c3(ACTIVE(a))
ACTIVE(b) → c1(MARK(a))
MARK(b) → c4(ACTIVE(b))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

ACTIVE(f(z0, z0)) → c(MARK(f(a, b)), F(a, b))
MARK(f(z0, z1)) → c2(ACTIVE(f(mark(z0), z1)), F(mark(z0), z1), MARK(z0))
F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
S tuples:

ACTIVE(f(z0, z0)) → c(MARK(f(a, b)), F(a, b))
MARK(f(z0, z1)) → c2(ACTIVE(f(mark(z0), z1)), F(mark(z0), z1), MARK(z0))
F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
K tuples:none
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, MARK, F

Compound Symbols:

c, c2, c5, c6, c7, c8

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
We considered the (Usable) Rules:

mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
f(z0, mark(z1)) → f(z0, z1)
f(mark(z0), z1) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
And the Tuples:

ACTIVE(f(z0, z0)) → c(MARK(f(a, b)), F(a, b))
MARK(f(z0, z1)) → c2(ACTIVE(f(mark(z0), z1)), F(mark(z0), z1), MARK(z0))
F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1, x2)) = x2   
POL(MARK(x1)) = [4]x1   
POL(a) = 0   
POL(active(x1)) = [5] + [4]x1   
POL(b) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c2(x1, x2, x3)) = x1 + x2 + x3   
POL(c5(x1)) = x1   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(f(x1, x2)) = x1 + [4]x2   
POL(mark(x1)) = [1] + [2]x1   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

ACTIVE(f(z0, z0)) → c(MARK(f(a, b)), F(a, b))
MARK(f(z0, z1)) → c2(ACTIVE(f(mark(z0), z1)), F(mark(z0), z1), MARK(z0))
F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
S tuples:

ACTIVE(f(z0, z0)) → c(MARK(f(a, b)), F(a, b))
MARK(f(z0, z1)) → c2(ACTIVE(f(mark(z0), z1)), F(mark(z0), z1), MARK(z0))
F(mark(z0), z1) → c5(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
K tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, MARK, F

Compound Symbols:

c, c2, c5, c6, c7, c8

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(f(z0, z0)) → c(MARK(f(a, b)), F(a, b)) by

ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

MARK(f(z0, z1)) → c2(ACTIVE(f(mark(z0), z1)), F(mark(z0), z1), MARK(z0))
F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
S tuples:

MARK(f(z0, z1)) → c2(ACTIVE(f(mark(z0), z1)), F(mark(z0), z1), MARK(z0))
F(mark(z0), z1) → c5(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
K tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

MARK, F, ACTIVE

Compound Symbols:

c2, c5, c6, c7, c8, c

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(f(z0, z1)) → c2(ACTIVE(f(mark(z0), z1)), F(mark(z0), z1), MARK(z0)) by

MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
S tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
K tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

F, ACTIVE, MARK

Compound Symbols:

c5, c6, c7, c8, c, c2, c2

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
We considered the (Usable) Rules:

mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
f(z0, mark(z1)) → f(z0, z1)
f(mark(z0), z1) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
And the Tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1, x2)) = 0   
POL(MARK(x1)) = x1   
POL(a) = 0   
POL(active(x1)) = 0   
POL(b) = [2]   
POL(c(x1)) = x1   
POL(c2(x1)) = x1   
POL(c2(x1, x2, x3)) = x1 + x2 + x3   
POL(c5(x1)) = x1   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(f(x1, x2)) = [4]x1   
POL(mark(x1)) = [4]x1   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
S tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
K tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

F, ACTIVE, MARK

Compound Symbols:

c5, c6, c7, c8, c, c2, c2

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
We considered the (Usable) Rules:

mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
f(z0, mark(z1)) → f(z0, z1)
f(mark(z0), z1) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
And the Tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = [1]   
POL(F(x1, x2)) = x2   
POL(MARK(x1)) = x1   
POL(a) = 0   
POL(active(x1)) = [2]x1   
POL(b) = 0   
POL(c(x1)) = x1   
POL(c2(x1)) = x1   
POL(c2(x1, x2, x3)) = x1 + x2 + x3   
POL(c5(x1)) = x1   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(f(x1, x2)) = [1] + [2]x1 + [2]x2   
POL(mark(x1)) = [4] + x1   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
S tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a))
K tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

F, ACTIVE, MARK

Compound Symbols:

c5, c6, c7, c8, c, c2, c2

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1))) by

MARK(f(f(x0, x1), z1)) → c2(ACTIVE(f(f(mark(x0), x1), z1)), F(mark(f(x0, x1)), z1), MARK(f(x0, x1)))
MARK(f(f(z0, z1), x2)) → c2(ACTIVE(f(active(f(z0, z1)), x2)), F(mark(f(z0, z1)), x2), MARK(f(z0, z1)))
MARK(f(f(f(z0, z1), x1), x2)) → c2(ACTIVE(f(active(f(active(f(mark(z0), z1)), x1)), x2)), F(mark(f(f(z0, z1), x1)), x2), MARK(f(f(z0, z1), x1)))
MARK(f(f(a, x1), x2)) → c2(ACTIVE(f(active(f(active(a), x1)), x2)), F(mark(f(a, x1)), x2), MARK(f(a, x1)))
MARK(f(f(b, x1), x2)) → c2(ACTIVE(f(active(f(active(b), x1)), x2)), F(mark(f(b, x1)), x2), MARK(f(b, x1)))
MARK(f(f(x0, x1), x2)) → c2(F(mark(f(x0, x1)), x2))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(f(x0, x1), z1)) → c2(ACTIVE(f(f(mark(x0), x1), z1)), F(mark(f(x0, x1)), z1), MARK(f(x0, x1)))
MARK(f(f(z0, z1), x2)) → c2(ACTIVE(f(active(f(z0, z1)), x2)), F(mark(f(z0, z1)), x2), MARK(f(z0, z1)))
MARK(f(f(f(z0, z1), x1), x2)) → c2(ACTIVE(f(active(f(active(f(mark(z0), z1)), x1)), x2)), F(mark(f(f(z0, z1), x1)), x2), MARK(f(f(z0, z1), x1)))
MARK(f(f(a, x1), x2)) → c2(ACTIVE(f(active(f(active(a), x1)), x2)), F(mark(f(a, x1)), x2), MARK(f(a, x1)))
MARK(f(f(b, x1), x2)) → c2(ACTIVE(f(active(f(active(b), x1)), x2)), F(mark(f(b, x1)), x2), MARK(f(b, x1)))
MARK(f(f(x0, x1), x2)) → c2(F(mark(f(x0, x1)), x2))
S tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a))
K tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

F, ACTIVE, MARK

Compound Symbols:

c5, c6, c7, c8, c, c2, c2

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(f(a, x1)) → c2(ACTIVE(f(active(a), x1)), F(mark(a), x1), MARK(a)) by

MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
MARK(f(a, x0)) → c2(F(mark(a), x0))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(f(x0, x1), z1)) → c2(ACTIVE(f(f(mark(x0), x1), z1)), F(mark(f(x0, x1)), z1), MARK(f(x0, x1)))
MARK(f(f(z0, z1), x2)) → c2(ACTIVE(f(active(f(z0, z1)), x2)), F(mark(f(z0, z1)), x2), MARK(f(z0, z1)))
MARK(f(f(f(z0, z1), x1), x2)) → c2(ACTIVE(f(active(f(active(f(mark(z0), z1)), x1)), x2)), F(mark(f(f(z0, z1), x1)), x2), MARK(f(f(z0, z1), x1)))
MARK(f(f(a, x1), x2)) → c2(ACTIVE(f(active(f(active(a), x1)), x2)), F(mark(f(a, x1)), x2), MARK(f(a, x1)))
MARK(f(f(b, x1), x2)) → c2(ACTIVE(f(active(f(active(b), x1)), x2)), F(mark(f(b, x1)), x2), MARK(f(b, x1)))
MARK(f(f(x0, x1), x2)) → c2(F(mark(f(x0, x1)), x2))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
MARK(f(a, x0)) → c2(F(mark(a), x0))
S tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
MARK(f(a, x0)) → c2(F(mark(a), x0))
K tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

F, ACTIVE, MARK

Compound Symbols:

c5, c6, c7, c8, c, c2, c2

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MARK(f(a, x0)) → c2(F(mark(a), x0))
We considered the (Usable) Rules:

mark(a) → active(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(b) → active(b)
active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
f(z0, mark(z1)) → f(z0, z1)
f(mark(z0), z1) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
And the Tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(f(x0, x1), z1)) → c2(ACTIVE(f(f(mark(x0), x1), z1)), F(mark(f(x0, x1)), z1), MARK(f(x0, x1)))
MARK(f(f(z0, z1), x2)) → c2(ACTIVE(f(active(f(z0, z1)), x2)), F(mark(f(z0, z1)), x2), MARK(f(z0, z1)))
MARK(f(f(f(z0, z1), x1), x2)) → c2(ACTIVE(f(active(f(active(f(mark(z0), z1)), x1)), x2)), F(mark(f(f(z0, z1), x1)), x2), MARK(f(f(z0, z1), x1)))
MARK(f(f(a, x1), x2)) → c2(ACTIVE(f(active(f(active(a), x1)), x2)), F(mark(f(a, x1)), x2), MARK(f(a, x1)))
MARK(f(f(b, x1), x2)) → c2(ACTIVE(f(active(f(active(b), x1)), x2)), F(mark(f(b, x1)), x2), MARK(f(b, x1)))
MARK(f(f(x0, x1), x2)) → c2(F(mark(f(x0, x1)), x2))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
MARK(f(a, x0)) → c2(F(mark(a), x0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = [4] + [3]x1   
POL(F(x1, x2)) = 0   
POL(MARK(x1)) = [4]x1   
POL(a) = 0   
POL(active(x1)) = x1   
POL(b) = 0   
POL(c(x1)) = x1   
POL(c2(x1)) = x1   
POL(c2(x1, x2, x3)) = x1 + x2 + x3   
POL(c5(x1)) = x1   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(f(x1, x2)) = [4] + [4]x1   
POL(mark(x1)) = x1   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(f(x0, x1), z1)) → c2(ACTIVE(f(f(mark(x0), x1), z1)), F(mark(f(x0, x1)), z1), MARK(f(x0, x1)))
MARK(f(f(z0, z1), x2)) → c2(ACTIVE(f(active(f(z0, z1)), x2)), F(mark(f(z0, z1)), x2), MARK(f(z0, z1)))
MARK(f(f(f(z0, z1), x1), x2)) → c2(ACTIVE(f(active(f(active(f(mark(z0), z1)), x1)), x2)), F(mark(f(f(z0, z1), x1)), x2), MARK(f(f(z0, z1), x1)))
MARK(f(f(a, x1), x2)) → c2(ACTIVE(f(active(f(active(a), x1)), x2)), F(mark(f(a, x1)), x2), MARK(f(a, x1)))
MARK(f(f(b, x1), x2)) → c2(ACTIVE(f(active(f(active(b), x1)), x2)), F(mark(f(b, x1)), x2), MARK(f(b, x1)))
MARK(f(f(x0, x1), x2)) → c2(F(mark(f(x0, x1)), x2))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
MARK(f(a, x0)) → c2(F(mark(a), x0))
S tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
K tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(a, x0)) → c2(F(mark(a), x0))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

F, ACTIVE, MARK

Compound Symbols:

c5, c6, c7, c8, c, c2, c2

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b)) by

MARK(f(b, z1)) → c2(ACTIVE(f(b, z1)), F(mark(b), z1), MARK(b))
MARK(f(b, x0)) → c2(ACTIVE(f(mark(a), x0)), F(mark(b), x0), MARK(b))
MARK(f(b, x0)) → c2

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(f(x0, x1), z1)) → c2(ACTIVE(f(f(mark(x0), x1), z1)), F(mark(f(x0, x1)), z1), MARK(f(x0, x1)))
MARK(f(f(z0, z1), x2)) → c2(ACTIVE(f(active(f(z0, z1)), x2)), F(mark(f(z0, z1)), x2), MARK(f(z0, z1)))
MARK(f(f(f(z0, z1), x1), x2)) → c2(ACTIVE(f(active(f(active(f(mark(z0), z1)), x1)), x2)), F(mark(f(f(z0, z1), x1)), x2), MARK(f(f(z0, z1), x1)))
MARK(f(f(a, x1), x2)) → c2(ACTIVE(f(active(f(active(a), x1)), x2)), F(mark(f(a, x1)), x2), MARK(f(a, x1)))
MARK(f(f(b, x1), x2)) → c2(ACTIVE(f(active(f(active(b), x1)), x2)), F(mark(f(b, x1)), x2), MARK(f(b, x1)))
MARK(f(f(x0, x1), x2)) → c2(F(mark(f(x0, x1)), x2))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
MARK(f(a, x0)) → c2(F(mark(a), x0))
MARK(f(b, z1)) → c2(ACTIVE(f(b, z1)), F(mark(b), z1), MARK(b))
MARK(f(b, x0)) → c2(ACTIVE(f(mark(a), x0)), F(mark(b), x0), MARK(b))
MARK(f(b, x0)) → c2
S tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
K tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
MARK(f(b, x1)) → c2(ACTIVE(f(active(b), x1)), F(mark(b), x1), MARK(b))
MARK(f(f(z0, z1), x1)) → c2(ACTIVE(f(active(f(mark(z0), z1)), x1)), F(mark(f(z0, z1)), x1), MARK(f(z0, z1)))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(a, x0)) → c2(F(mark(a), x0))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

F, ACTIVE, MARK

Compound Symbols:

c5, c6, c7, c8, c, c2, c2, c2

(23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

MARK(f(b, x0)) → c2

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(f(x0, x1), z1)) → c2(ACTIVE(f(f(mark(x0), x1), z1)), F(mark(f(x0, x1)), z1), MARK(f(x0, x1)))
MARK(f(f(z0, z1), x2)) → c2(ACTIVE(f(active(f(z0, z1)), x2)), F(mark(f(z0, z1)), x2), MARK(f(z0, z1)))
MARK(f(f(f(z0, z1), x1), x2)) → c2(ACTIVE(f(active(f(active(f(mark(z0), z1)), x1)), x2)), F(mark(f(f(z0, z1), x1)), x2), MARK(f(f(z0, z1), x1)))
MARK(f(f(a, x1), x2)) → c2(ACTIVE(f(active(f(active(a), x1)), x2)), F(mark(f(a, x1)), x2), MARK(f(a, x1)))
MARK(f(f(b, x1), x2)) → c2(ACTIVE(f(active(f(active(b), x1)), x2)), F(mark(f(b, x1)), x2), MARK(f(b, x1)))
MARK(f(f(x0, x1), x2)) → c2(F(mark(f(x0, x1)), x2))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
MARK(f(a, x0)) → c2(F(mark(a), x0))
MARK(f(b, z1)) → c2(ACTIVE(f(b, z1)), F(mark(b), z1), MARK(b))
MARK(f(b, x0)) → c2(ACTIVE(f(mark(a), x0)), F(mark(b), x0), MARK(b))
S tuples:

F(mark(z0), z1) → c5(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
K tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(a, x0)) → c2(F(mark(a), x0))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

F, ACTIVE, MARK

Compound Symbols:

c5, c6, c7, c8, c, c2, c2

(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(mark(z0), z1) → c5(F(z0, z1)) by

F(mark(mark(y0)), z1) → c5(F(mark(y0), z1))
F(mark(z0), mark(y1)) → c5(F(z0, mark(y1)))
F(mark(active(y0)), z1) → c5(F(active(y0), z1))
F(mark(z0), active(y1)) → c5(F(z0, active(y1)))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(f(x0, x1), z1)) → c2(ACTIVE(f(f(mark(x0), x1), z1)), F(mark(f(x0, x1)), z1), MARK(f(x0, x1)))
MARK(f(f(z0, z1), x2)) → c2(ACTIVE(f(active(f(z0, z1)), x2)), F(mark(f(z0, z1)), x2), MARK(f(z0, z1)))
MARK(f(f(f(z0, z1), x1), x2)) → c2(ACTIVE(f(active(f(active(f(mark(z0), z1)), x1)), x2)), F(mark(f(f(z0, z1), x1)), x2), MARK(f(f(z0, z1), x1)))
MARK(f(f(a, x1), x2)) → c2(ACTIVE(f(active(f(active(a), x1)), x2)), F(mark(f(a, x1)), x2), MARK(f(a, x1)))
MARK(f(f(b, x1), x2)) → c2(ACTIVE(f(active(f(active(b), x1)), x2)), F(mark(f(b, x1)), x2), MARK(f(b, x1)))
MARK(f(f(x0, x1), x2)) → c2(F(mark(f(x0, x1)), x2))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
MARK(f(a, x0)) → c2(F(mark(a), x0))
MARK(f(b, z1)) → c2(ACTIVE(f(b, z1)), F(mark(b), z1), MARK(b))
MARK(f(b, x0)) → c2(ACTIVE(f(mark(a), x0)), F(mark(b), x0), MARK(b))
F(mark(mark(y0)), z1) → c5(F(mark(y0), z1))
F(mark(z0), mark(y1)) → c5(F(z0, mark(y1)))
F(mark(active(y0)), z1) → c5(F(active(y0), z1))
F(mark(z0), active(y1)) → c5(F(z0, active(y1)))
S tuples:

F(active(z0), z1) → c7(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
F(mark(mark(y0)), z1) → c5(F(mark(y0), z1))
F(mark(z0), mark(y1)) → c5(F(z0, mark(y1)))
F(mark(active(y0)), z1) → c5(F(active(y0), z1))
F(mark(z0), active(y1)) → c5(F(z0, active(y1)))
K tuples:

F(z0, mark(z1)) → c6(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(a, x0)) → c2(F(mark(a), x0))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

F, ACTIVE, MARK

Compound Symbols:

c6, c7, c8, c, c2, c2, c5

(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(z0, mark(z1)) → c6(F(z0, z1)) by

F(z0, mark(mark(y1))) → c6(F(z0, mark(y1)))
F(active(y0), mark(z1)) → c6(F(active(y0), z1))
F(z0, mark(active(y1))) → c6(F(z0, active(y1)))
F(mark(mark(y0)), mark(z1)) → c6(F(mark(mark(y0)), z1))
F(mark(y0), mark(mark(y1))) → c6(F(mark(y0), mark(y1)))
F(mark(active(y0)), mark(z1)) → c6(F(mark(active(y0)), z1))
F(mark(y0), mark(active(y1))) → c6(F(mark(y0), active(y1)))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
mark(f(z0, z1)) → active(f(mark(z0), z1))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1) → f(z0, z1)
f(z0, mark(z1)) → f(z0, z1)
f(active(z0), z1) → f(z0, z1)
f(z0, active(z1)) → f(z0, z1)
Tuples:

F(active(z0), z1) → c7(F(z0, z1))
F(z0, active(z1)) → c8(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(f(x0, x1), z1)) → c2(ACTIVE(f(f(mark(x0), x1), z1)), F(mark(f(x0, x1)), z1), MARK(f(x0, x1)))
MARK(f(f(z0, z1), x2)) → c2(ACTIVE(f(active(f(z0, z1)), x2)), F(mark(f(z0, z1)), x2), MARK(f(z0, z1)))
MARK(f(f(f(z0, z1), x1), x2)) → c2(ACTIVE(f(active(f(active(f(mark(z0), z1)), x1)), x2)), F(mark(f(f(z0, z1), x1)), x2), MARK(f(f(z0, z1), x1)))
MARK(f(f(a, x1), x2)) → c2(ACTIVE(f(active(f(active(a), x1)), x2)), F(mark(f(a, x1)), x2), MARK(f(a, x1)))
MARK(f(f(b, x1), x2)) → c2(ACTIVE(f(active(f(active(b), x1)), x2)), F(mark(f(b, x1)), x2), MARK(f(b, x1)))
MARK(f(f(x0, x1), x2)) → c2(F(mark(f(x0, x1)), x2))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
MARK(f(a, x0)) → c2(F(mark(a), x0))
MARK(f(b, z1)) → c2(ACTIVE(f(b, z1)), F(mark(b), z1), MARK(b))
MARK(f(b, x0)) → c2(ACTIVE(f(mark(a), x0)), F(mark(b), x0), MARK(b))
F(mark(mark(y0)), z1) → c5(F(mark(y0), z1))
F(mark(z0), mark(y1)) → c5(F(z0, mark(y1)))
F(mark(active(y0)), z1) → c5(F(active(y0), z1))
F(mark(z0), active(y1)) → c5(F(z0, active(y1)))
F(z0, mark(mark(y1))) → c6(F(z0, mark(y1)))
F(active(y0), mark(z1)) → c6(F(active(y0), z1))
F(z0, mark(active(y1))) → c6(F(z0, active(y1)))
F(mark(mark(y0)), mark(z1)) → c6(F(mark(mark(y0)), z1))
F(mark(y0), mark(mark(y1))) → c6(F(mark(y0), mark(y1)))
F(mark(active(y0)), mark(z1)) → c6(F(mark(active(y0)), z1))
F(mark(y0), mark(active(y1))) → c6(F(mark(y0), active(y1)))
S tuples:

F(active(z0), z1) → c7(F(z0, z1))
ACTIVE(f(x0, x0)) → c(MARK(f(a, b)))
MARK(f(z0, z1)) → c2(ACTIVE(f(z0, z1)), F(mark(z0), z1), MARK(z0))
MARK(f(a, z1)) → c2(ACTIVE(f(a, z1)), F(mark(a), z1), MARK(a))
F(mark(mark(y0)), z1) → c5(F(mark(y0), z1))
F(mark(z0), mark(y1)) → c5(F(z0, mark(y1)))
F(mark(active(y0)), z1) → c5(F(active(y0), z1))
F(mark(z0), active(y1)) → c5(F(z0, active(y1)))
K tuples:

F(z0, active(z1)) → c8(F(z0, z1))
MARK(f(x0, x1)) → c2(F(mark(x0), x1))
MARK(f(a, x0)) → c2(F(mark(a), x0))
F(z0, mark(mark(y1))) → c6(F(z0, mark(y1)))
F(active(y0), mark(z1)) → c6(F(active(y0), z1))
F(z0, mark(active(y1))) → c6(F(z0, active(y1)))
F(mark(mark(y0)), mark(z1)) → c6(F(mark(mark(y0)), z1))
F(mark(y0), mark(mark(y1))) → c6(F(mark(y0), mark(y1)))
F(mark(active(y0)), mark(z1)) → c6(F(mark(active(y0)), z1))
F(mark(y0), mark(active(y1))) → c6(F(mark(y0), active(y1)))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

F, ACTIVE, MARK

Compound Symbols:

c7, c8, c, c2, c2, c5, c6

(29) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match(-raise)-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 3.

The compatible tree automaton used to show the Match(-raise)-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 11]
transitions:
active0(0) → 1
mark0(0) → 2
f0(0, 0) → 3
mark1(4) → 1
active1(5) → 2
b1() → 6
active1(6) → 2
b1() → 0
b1() → 8
active0(7) → 1
active0(8) → 1
mark0(7) → 2
mark0(8) → 2
f0(7, 0) → 3
f0(0, 7) → 3
f0(8, 0) → 3
f0(0, 8) → 3
f0(7, 7) → 3
f0(7, 8) → 3
f0(8, 7) → 3
f0(8, 8) → 3
mark1(7) → 1
active1(7) → 2
active1(8) → 2
active1(7) → 1
active1(8) → 1
mark1(7) → 2
mark2(9) → 2
active2(10) → 1
mark1(7) → 11
active1(7) → 11
active1(8) → 11
active0(12) → 1
mark0(12) → 2
f0(12, 0) → 3
f0(12, 7) → 3
f0(12, 8) → 3
f0(0, 12) → 3
f0(7, 12) → 3
f0(8, 12) → 3
f0(12, 12) → 3
mark1(12) → 11
active1(12) → 11
mark2(12) → 2
active2(12) → 1
active1(12) → 1
mark1(12) → 2
mark2(12) → 11
active2(12) → 11
a3() → 13
active3(13) → 2
a3() → 9
a3() → 4
a3() → 0
a3() → 5
a3() → 7
a3() → 10
a3() → 12
a3() → 14
active0(14) → 1
mark0(14) → 2
f0(14, 0) → 3
f0(14, 7) → 3
f0(14, 8) → 3
f0(14, 12) → 3
f0(0, 14) → 3
f0(7, 14) → 3
f0(8, 14) → 3
f0(12, 14) → 3
f0(14, 14) → 3
mark1(14) → 11
active1(14) → 11
mark2(14) → 11
active2(14) → 11
active3(14) → 2
active1(14) → 1
active2(14) → 1
active3(14) → 1
mark1(14) → 2
mark2(14) → 2
active3(14) → 11

(30) BOUNDS(O(1), O(n^1))